sendMinimalR{$a:ut2, $tg:ut2}
sendMinimalR(T; l; ds1; ds2; P; Q; f)
== ([at src(l):
== ([action $a(m) 
== ([precondition s,m. P(s,m) & (n:. n<m  P(s,n))
== ([psends [$tg,f] on link l
== (; at src(lnk-inv(l)):
== (; action $a(m) 
== (; precondition s,m. Q(s,m) & (n:. n<m  Q(s,n))
== (; psends [$tg,s,m. m] on link lnk-inv(l)]) 

latex

---

clarification:

sendMinimalR{$a:ut2, $tg:ut2}
sendMinimalR(T; l; ds1; ds2; P; Q; f)
== (weakPrecondSendR{$a,$tg}(T;;l;ds1;s,m. P(s,m) & (n:. n<m  P(s,n));f)
== (.weakPrecondSendR{$a,$tg}(;;lnk-inv(l);ds2;s,m. Q(s,m) & (n:. n<m  Q(s,n));s,m. m)
== (..nil) 

latex

Definitions

(L), car.cdr, at src(l):action $a(m) precondition P sends [$tg,f] on link l, lnk-inv(l), P & Q, A, x:A. B(x), , P  Q, a<b, f(a), x.A(x), nil